%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%
%% Basic Definitions and Macros 
%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%
%% Authors: Carlos Olarte, Elaine Pimentel
%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%   Packages required  %%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\usepackage{amssymb}
%\usepackage{amsmath}
%\usepackage{latexsym}
%\usepackage{proof}
%\usepackage{myproof}
%\usepackage{stmaryrd}
%\usepackage{hyphenat}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%\newtheorem{proposition}[theorem]{Proposition}

%Defined macros

%Andreoli's focusing system

\newcommand{\Up}[3]{#1;#2\Uparrow #3}
\newcommand{\Down}[3]{#1;#2\Downarrow #3}
\newcommand{\nng}[1]{#1^\perp}

%Vivek's multimodal systems

\DeclareMathAlphabet{\mathsl}{OT1}{cmr}{m}{sl}

\newcommand\eg{\hbox{\textit{e.g.}}}
\newcommand\ie{\hbox{\textit{i.e.}}}

\newcommand{\rfoc}[1]{-_{#1}\!\!\to}
%\newcommand{\lfoc}[1]{\stackrel {#1} {\longrightarrow}}
\newcommand{\lfoc}[1]{\xrightarrow{#1}}
\newcommand{\LJF}{\hbox{\sl LJF}}
\newcommand{\LKF}{\hbox{\sl LKF}}
\newcommand{\false}{\hbox{\sl false}}
\newcommand{\idPa}[1]{\mathcal{T}\left( #1 \right)}


\newcommand\llfDash{\vdash}
\newcommand\ndDash{\vdash_{\mathsl{nd}}}
\newcommand\ncmDash{\vdash}
\newcommand\lEncBpG{\mathcal{P}_{bp}^\mathcal{G}}
\newcommand\lEncDjks{\mathcal{P}_{dj}^\mathcal{G}}
\newcommand\lEnc{\mathcal{L}}
\newcommand\mljDash{\vdash_{\mathsl{mlj}}}
\newcommand\ljqDash{\vdash_{\mathsl{ljq}}}
\newcommand\mfDash{\vdash_{\mathsl{mf}}}
\newcommand\ljqfDash{\rightarrow_{\mathsl{ljq}}}
%\newcommand\ljqfDash{\rightarrow_{\hbox{\sl ljq}}}
\newcommand\gImDash{\vdash_{\mathsl{g1m}}}
\newcommand\gIiDash{\vdash_{\mathsl{g1i}}}
\newcommand\gIcDash{\vdash_{\mathsl{g1c}}}
\newcommand\gIIImDash{\vdash_{\mathsl{g3m}}}
\newcommand\gIIIiDash{\vdash_{\mathsl{g3i}}}
\newcommand\gIIIcDash{\vdash_{\mathsl{g3c}}}
\newcommand\lEncMLJ{\lEnc_{\mathsl{mlj}}}
\newcommand\lEncGi{\lEnc_{\mathsl{gi}}}
\newcommand\lEncGIm{\lEnc_{\mathsl{g1m}}}
\newcommand\lEncGIi{\lEnc_{\mathsl{g1i}}}
\newcommand\lEncGIc{\lEnc_{\mathsl{g1c}}}
\newcommand\lEncGIII{\lEnc_{\mathsl{g3}}}
\newcommand\lEncGIIIM{\lEnc_{\mathsl{g3m}}}
\newcommand\lEncGIIIJ{\lEnc_{\mathsl{g3i}}}
\newcommand\lEncGIIIC{\lEnc_{\mathsl{g3c}}}
\newcommand\lEncLJF{\lEnc_{{\mathsl{ljf}}}}
\newcommand\lEncLKF{\lEnc_{\mathsl{lkf}}}
\newcommand\lEncMF{\lEnc_{\mathsl{mf}}}
\newcommand\lEncLJQ{\lEnc_{\mathsl{ljq}}}
\newcommand\lkfDashU{\vdash_{\mathsl{lkf}}}
\newcommand\lkfDashF{\mapsto_{\mathsl{lkf}}}

%Sequent systems
\newcommand\LJ{\textbf{LJ}}
\newcommand\LK{\textbf{LK}}
\newcommand\LL{\textbf{LL}}
\newcommand\LU{\textbf{LU}}
\newcommand\LM{\textbf{LM}}
\newcommand\NM{\textbf{NM}}
\newcommand\ILU{\textbf{ILU}}
\newcommand\FLL{\textbf{FLL}}
\newcommand\IIL{\textbf{IIL}}
\newcommand\IILs{\textbf{IIL*}}
\newcommand\LJp{\textbf{LJ'}}
\newcommand\LKQ{\textbf{LKQ}}
\newcommand\LJQ{\textbf{LJQ}}
\newcommand\LKT{\textbf{LKT}}
\newcommand\LJK{\textbf{LJK}}
\newcommand\LMone{\textbf{LM1}}
\newcommand\LC{\textbf{LC}}
\newcommand\LI{\textbf{LI}}
\newcommand\LMC{\textbf{LMC}}
\newcommand\LJN{\textbf{LJN}}
\newcommand\Gtc{\textbf{G3c}}
\newcommand\mLJ{\textbf{mLJ}}

\newcommand\LKdef{\Lscr\Kscr}
\newcommand\LJdef{\Lscr\Jscr}
\newcommand\LLdef{\Lscr\Lscr}
%\newcommand\ILUdef{\Iscr\Lscr\Uscr}
%\newcommand\LKQdef{\Lscr\Kscr\Qscr}
%\newcommand\LKTdef{\Lscr\Kscr\Tscr}

%Named clauses
\newcommand\Cut{\hbox{\sl Cut}}
\newcommand\Init{\hbox{\sl Init}}
\newcommand\ACut{\hbox{\sl ACut}}
\newcommand\AInit{\hbox{\sl AInit}}
\newcommand\Neg{\hbox{\sl Neg}}
\newcommand\Pos{\hbox{\sl Pos}}
\newcommand\ANeg{\hbox{\sl ANeg}}
\newcommand\APos{\hbox{\sl APos}}

\newcommand\Aneg[1]{\hbox{\sl Aneg}(#1)}
\newcommand\Apos[1]{\hbox{\sl Apos}(#1)}
\newcommand\Aneu[1]{\hbox{\sl Aneu}(#1)}

%Atomic predicates
\newcommand\atomic[1]{{\hbox{\sl atomic}}(#1)}
\newcommand\formula[1]{{\hbox{\sl formula}}(#1)}
\newcommand\rght[1]{\lceil #1 \rceil}
\newcommand\lft[1]{\lfloor #1 \rfloor}
\newcommand\ngp[1]{#1^\perp}

%Other macros
\newcommand\PEYE{\Pi}
%\newcommand\bool{\hbox{\sl bool}}
\newcommand\allhat{\hat\forall}
\newcommand\Fife[5]{#1;#2\mathrel{\buildrel #3\over\longrightarrow}#4;#5}
\newcommand\Fifex[6]{#1;#2\mathrel{\buildrel #3\over{\hbox to #6pt{\rightarrowfill}}}#4;#5}
\newcommand\Foor[4]{#1;#2\longrightarrow#3;#4}
\newcommand\Four[5]{#1\colon #2;#3\longrightarrow#4;#5}
\newcommand\Lred[3]{#1\;{\mathrel{\buildrel #2\over\Longrightarrow} #3}}
\newcommand\Red[2]{#1\Longrightarrow #2}
\newcommand\seq[3]{#1:#2\longrightarrow #3}
\newcommand\Seq[2]{#1\longrightarrow #2}
\newcommand\seqLKT[3]{#1;#2\longrightarrow #3}
\newcommand\seqLKQ[3]{#1\longrightarrow #2; #3}
\newcommand\somehat{\hat\exists}
\newcommand\lp{$\lambda$Prolog}
\newcommand\ppar{\mathbin{\vert}}
\newcommand\red[3]{#1;#2\Longrightarrow #3}
\newcommand\redstar[3]{#1;#2\Longrightarrow^{*} #3}
\newcommand\sred[3]{#1;#2{\mathrel{\buildrel\tau\over\Longrightarrow} #3}}
\newcommand\sseq{\seq\Sigma{\Delta}}
\newcommand\trans[1]{\langle\!\langle#1\rangle\!\rangle}
\newcommand\veq{\mathrel{\dashv\vdash}}
\newcommand\xFour[4]{#1;#2\longrightarrow#3;#4}
\newcommand\xFive[5]{#1;#2\mathrel{\buildrel #3\over\longrightarrow}#4;#5}

%Mathcal
\newcommand\mA{{\mathcal A}}
\newcommand\mB{{\mathcal B}}
\newcommand\mM{{\mathcal M}}
\newcommand\mN{{\mathcal N}}
\newcommand\mD{{\mathcal D}}
\newcommand\mG{{\mathcal G}}
\newcommand\mP{{\mathcal P}}
\newcommand\mQ{{\mathcal Q}}

%Special arrows
\newcommand\ra\rightarrow
\newcommand\rimp{\Leftarrow}

% Object-level type (not bool anymore)
\newcommand{\obj}{\hbox{\sl obj}}

%Intuitionistic constants
\newcommand\iand{\cap}
\newcommand\ior{\cup}
\newcommand\iimp{\supset}
\newcommand\ifalse{f_{i}}
\newcommand\itrue{t_{i}}
\newcommand\iforall{\forall_{i}}
\newcommand\iexists{\exists_{i}}

%Classical constants
\newcommand\cand{\wedge}
\newcommand\cor{\lor}
\newcommand\cimp{\Rightarrow}
\newcommand\cfalse{f_{c}}
\newcommand\ctrue{t_{c}}
\newcommand\cforall{\forall_{c}}
\newcommand\cexists{\exists_{c}}

%Linear constants
\newcommand\zero{0}
\newcommand\one{1}
\newcommand\bottom{\perp}
\newcommand\bang{\mathop{!}}
\newcommand\quest{\mathord{?}}
%\newcommand\quest{\mathop{?}}
\newcommand\limp{\mathbin{-\hspace{-0.70mm}\circ}}
\newcommand\tensor\otimes
%\newcommand\with{\mathbin{\&}}
\newcommand\with{\binampersand}
\newcommand\bla{\mathrel{\mbox{$\circ\!-$}}}
\newcommand\lforall{\forall_{l}}
\newcommand\lexists{\exists_{l}}

%LU constants
\newcommand\pos[1]{\hbox{\sl pos}(#1)}
\newcommand\ngg[1]{\hbox{\sl neg}(#1)}
\newcommand\neu[1]{\hbox{\sl neu}(#1)}
\newcommand\notpos[1]{\hbox{\sl npos}(#1)}  % shortened the name
\newcommand\notngg[1]{\hbox{\sl nneg}(#1)}  % shortened the name
\newcommand\notneu[1]{\hbox{\sl nneu}(#1)}  % shortened the name
\newcommand\class[1]{\hbox{\sl classical}(#1)}

%Induction constants
\newcommand{\oo}{\hbox{\sl o}}
\newcommand{\nt}{\hbox{\sl nt}}
\newcommand\nat[1]{\hbox{\sl nat} \; #1}
\newcommand\z{\hbox{\sl z}}
\newcommand\suc[1]{\hbox{\sl s} \; #1}
\newcommand\natR{\hbox{\sl nat}{\cal R}}
\newcommand\natL{\hbox{\sl nat}{\cal L}}
\newcommand\FOLDN{FO\lambda^{\Delta\N}}
\newcommand\FF{\hbox{\sl Llinda}}
\newcommand{\N}{{\rm I} \! {\rm N}}


%Formula induction predicates and rules
\newcommand\iform[1]{\hbox{\sl form}_{i}(#1)}
\newcommand\kform[1]{\hbox{\sl form}_{k}(#1)}
\newcommand\Lform[1]{\hbox{\sl form}_{L}(#1)}
\newcommand\form[1]{\hbox{\sl form}(#1)}
\newcommand\iformR{\hbox{\sl form}_{i}{\cal R}}
\newcommand\iformL{\hbox{\sl form}_{i}{\cal L}}
\newcommand\height[2]{\hbox{\sl height}(#1,#2)}
\newcommand\iproof[1]{\hbox{\sl proof}_{i}(#1)}
\newcommand\iproofR{\hbox{\sl proof}_{i}{\cal R}}
\newcommand\iproofL{\hbox{\sl proof}_{i}{\cal L}}

%Definitions
\newcommand\defc[4]{{\rm dfn}(#1,#2,#3,#4)}
\newcommand\defeq{\stackrel{\scriptscriptstyle\triangle}{=}}
\newcommand{\bdash}{\mathrel{\vrule\vdash}}
\newcommand\defR{\hbox{\sl def}{\cal R}}
\newcommand\defL{\hbox{\sl def}{\cal L}}
\newcommand\eqR{\hbox{\sl eq}{\cal R}}
\newcommand\eqL{\hbox{\sl eq}{\cal L}}
%\newcommand\indR{\hbox{\sl ind}{\cal R}}
\newcommand\indL{\mu\cal L}
\newcommand\lvl[1]{lvl(#1)}
\newcommand\rc[1]{rc(#1)}
\newcommand{\gdash}{\vdash\kern -4pt\vdash}
\newcommand{\gseq}[2]{#1\gdash#2}
\newcommand{\tr}{\triangleright}
\newcommand{\tl}{\triangleleft}
\newcommand{\trcf}{\triangleright_{cf}}
\renewcommand{\rhd}{\parallel} % Change this to the one I used with McDowell

\def\Ascr{{\cal A}}
\def\Bscr{{\cal B}}
\def\Cscr{{\cal C}}
\def\Dscr{{\cal D}}
\def\Escr{{\cal E}}
\def\Fscr{{\cal F}}
\def\Gscr{{\cal G}}
\def\Hscr{{\cal H}}
\def\Iscr{{\cal I}}
\def\Jscr{{\cal J}}
\def\Kscr{{\cal K}}
\def\Lscr{{\mathcal L}}
\def\Mscr{{\cal M}}
\def\Nscr{{\cal N}}
\def\Oscr{{\cal O}}
\def\Pscr{{\cal P}}
\def\Qscr{{\cal Q}}
\def\Rscr{{\cal R}}
\def\Sscr{{\cal S}}
\def\Tscr{{\cal T}}
\def\Uscr{{\cal U}}
\def\Vscr{{\cal V}}
\def\Wscr{{\cal W}}
\def\Xscr{{\cal X}}
\def\Yscr{{\cal Y}}
\def\Zscr{{\cal Z}}


%  \draw package.  Vaughan Pratt  (C) 1993
%
%	*+,-|.|/012	Table of 81 vectors in [-4,4]x[-4,4]
%	3456|7|89:;	Use as parameters to tell \draw how to step along
%	<=>?|@|ABCD	\draw zzzzzzz\end draws a straight line 7 steps
%	EFGH|I|JKLM	   down and to the right
%       ----+-+----
%	NOPQ|R|STUV	R = (0,0), C = (3,2), * = (-4,-4), r = (-4,4)
%       ----+-+----
%	WXYZ|[|\]^_	\draw -./9:CMV_gpowvukjaWNE=45\end
%	`abc|d|efgh	   draws a reasonable circle
%	ijkl|m|nopq
%	rstu|v|wxyz
%
\newcount\PLv\newcount\PLw\newcount\PLx\newcount\PLy\newdimen\PLyy\newdimen\PLX
\newbox\PLdot \setbox\PLdot\hbox{\tiny.} \def\scl{.08} % resettable scale
\def\PLot#1{\PLx`#1\advance\PLx-42\PLy\PLx\PLv\PLx\divide\PLy9\PLw\PLy\multiply
\PLw9\advance\PLx-\PLw\advance\PLx-4\PLy-\PLy\advance\PLy4\PLX=\the\PLx pt
\advance\PLyy\the\PLy pt\wd\PLdot=\scl\PLX\raise\scl\PLyy\copy\PLdot}
\def\draw#1{\ifx#1\end\let\next=\relax\else\PLot#1\let\next=\draw\fi\next}

%  Girard's inverted ampersand.  Usage: \invamp. Draw time @ 10 Mips: .33 sec
\def\invamp{\hbox{\PLyy=70pt\draw :::;DMV_gqppyyyyyooooxxxnnwvlutkjaWNE=5-./9%
9:::CCCC:::99/..--544=EENWWaajjjkktttttttNNNVVVVVVVV\end \hskip4pt}}
%  \Invamp = Boxed \invamp.  Draw time < .02 sec, but max ~300 chars/page
\newbox\iabox\setbox\iabox\invamp \def\Invamp{\copy\iabox}

\newcommand\lpar{\mathrel{\Invamp}}
%\newcommand\lpar{\mathbin{\wp}}  % Looks ugly
%\newcommand\lpar{\bindnasrepma}  % Needs stmaryrd.sty, not on all machines

\long\def\hide#1\endhide{}

\newcommand{\iimpL}{\mathord{\iimp}L}
\newcommand{\iimpR}{\mathord{\iimp}R}
\newcommand{\cimpL}{\mathord{\cimp}L}
\newcommand{\cimpR}{\mathord{\cimp}R}

% Other Vivek's commands



\newcommand{\forallLoc}{{\Cap}}
\newcommand{\existsLoc}{\Cup}

\newcommand\Def{\tsl{def}}

\newcommand{\notAnc}{\preceq_\mathsl{R}}
\newcommand{\notAncEq}{\preceqeq_\mathsl{R}}
\newcommand{\descen}{\preceq}
\newcommand{\descenEq}{\preceqeq}
\newcommand{\load}{\textbf{load}}
\newcommand{\unload}{\textbf{unload}}
%\newcommand{\case}{\textbf{case}}
\newcommand{\If}{\textbf{if}}
\newcommand{\eCase}{\textbf{endc}}
\newcommand{\while}{\textbf{while}}
\newcommand{\eWhile}{\textbf{endw}}
\newcommand{\eProgram}{\textbf{end}}
\newcommand{\eBound}{\textbf{endu}}
\newcommand{\eUloc}{\textbf{empty}}
\newcommand{\isEmpty}{\textbf{is\_empty}}
\newcommand{\loopLoc}{\textbf{loop}}
\newcommand{\openDef}{\textbf{open}}
%\newcommand{\instr}{\tsl{instr}}
%\newcommand{\binstr}{\tsl{binstr}}
\newcommand{\bprog}{\tsl{bprog}}
\newcommand{\kprog}{\tsl{kprog}}
\newcommand{\lprog}{\tsl{lprog}}
\newcommand{\kvar}{\tsl{Kvar}}
\newcommand{\prog}{\tsl{prog}}
\newcommand{\pat}{\tsl{pat}}
\newcommand{\module}{\tsl{mod}}
\newcommand{\cont}{\tsl{cont}}
\newcommand{\cond}{\tsl{cond}}
\newcommand{\paral}{\talloblong}
\newcommand{\deq}{\mathrel{\stackrel {\Delta} {=}}}
\newcommand{\newLoc}{\textbf{new}}

\newcommand{\delay}[1]{\hbox{$\delta^-{\left(#1\right)}$}}
\newcommand{\delayp}[1]{\hbox{$\delta^+{\left(#1\right)}$}}

\newcommand{\match}{\textsc{match}}
\newcommand{\inM}{\textsc{in}}
\newcommand{\exec}{\hbox{$\mathcal{D}$}}
\newcommand{\ccond}{\textsc{ccond}}
\newcommand{\inc}{\textsc{inc}}
\newcommand{\state}{\textsc{state}}
\newcommand{\rem}{\textsc{rem}}

\newcommand{\eLoc}[1]{e#1}

\newcommand{\rUp}{R\mathord{\Uparrow}}
\newcommand{\rDown}{R\mathord{\Downarrow}}


 \newcommand{\ndots}[1]{\stackrel{\vcenter{\hbox{$\scriptstyle :$}
 \vskip-.35ex}}{\hbox {$ \scriptstyle \mathsl{#1}$}}}

\newcommand{\nbang}[1]{\hbox{$\bang^\mathsl{#1}$}}
\newcommand{\nquest}[1]{\hbox{$\quest^\mathsl{#1}$}}
\newcommand{\maxSE}{{\scriptstyle\infty}}
\newcommand{\minSE}{{\scriptstyle-\infty}}
\newcommand{\maxBang}{\bang^\maxSE}


\newcommand{\ncLL}{\hbox{\sl SELL}}
\newcommand{\ncLLF}{\hbox{\sl SELLF}}
\newcommand{\ncLLM}{\hbox{{\sl SELL}$^-$}}
\newcommand{\ncLLN}{\hbox{{\sl SELL}$^{\Cap}$}}
\newcommand{\ncLLNS}{\hbox{{\sl SELL}$^{\Cap_l}$}}
\newcommand{\sell}{\hbox{\sl SELL}}
\newcommand{\sellf}{\hbox{\sl SELLF}}


\newcommand\cost[1]{\tsl{C}_{#1}}
\newcommand\prf[1]{\hbox{$\Upsilon_{#1}$}}

\newcommand\qw{\mathcal{W}}
\newcommand\qc{\mathcal{C}}


\DeclareMathAlphabet{\mathsl}{OT1}{cmr}{m}{sl}
\newcommand\tsl[1]{\hbox{$\mathsl{#1}$}}

\newcommand{\adj}{\tsl{adj}}
\newcommand{\node}{\tsl{node}}
\newcommand{\tup}[1]{\langle#1\rangle}
\newcommand{\cons}{\mathbin{::}}
\newcommand{\nil}{\hbox{nil}}
\newcommand{\rel}{\hbox{rel}}
\newcommand{\Name}{\textsc{Bag}} 

